/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package chameleon.model.formula;

import java.io.IOException;

/**
 * This operator manage the run in a formula of type Buchi Game. This formula
 * have the following syntax  : AND(GF proposition).
 */

/**
 *
 * @author simon
 */
public class BuchiGameIterator {

    private Formula formula_;
    private Formula currentFormula_;

    public BuchiGameIterator(Formula formula){
        formula_ = formula;
        currentFormula_ = formula_;
    }

    /**
     * Return a GF (boolean formula) on left of current AND operator.
     *
     * @return
     * @throws IOException
     */

    public Formula getBuchiFormula() throws IOException{
        // return the proposition of the current formula
        Formula exp_opt ;
        if (currentFormula_.getOperator().getTag() == Tag.AND){
            Formula always = currentFormula_.getLeftF(); // Always operator
            Formula eventually = always.getRightF(); //Eventually operator
            exp_opt = eventually.getRightF();
        }
        else{
            Formula eventually = currentFormula_.getRightF(); //Eventually operator
            exp_opt = eventually.getRightF();
        }
        return exp_opt;
    }

    /**
     * Return a GF (boolean formula) on right of current AND operator.
     *
     * @return
     * @throws IOException
     */

    public Formula getBuchiFormulaRight() throws IOException{
        // return the proposition of the current formula
        Formula always = currentFormula_.getRightF(); // Always operator
        Formula eventually = always.getRightF(); //Eventually operator
        Formula exp_opt = eventually.getRightF();
        return exp_opt;
    }

    public void next() throws IOException{
        //return the next and formula in the BuchiGame
        currentFormula_ = currentFormula_.getRightF();
    }

    public boolean hasNext() throws IOException{
        if (currentFormula_ != null && currentFormula_.getRightF() != null){
            Operator op = currentFormula_.getRightF().getOperator();
            return (op.isEquals(Tag.AND) || op.isEquals(Tag.ALWAYS) ) ;
        }
        else
            return false;
    }

}
